/*
 * Copyright (c) 2015—2030 GantSoftware.Co.Ltd. All rights reserved.
 *  <p>
 *  Unless required by applicable law or agreed to in writing, software
 *  is not allowed to be distributed or copied without the license from
 *  GantSoftware.Co.Ltd. Please contact the company for more information.
 */
package com.gantang.gax.engine.eo;

import cn.hutool.core.date.DateUtil;
import cn.hutool.core.date.TimeInterval;
import cn.hutool.core.lang.Console;
import cn.hutool.core.util.StrUtil;
import com.gantang.gax.engine.exception.EngineException;
import com.gantang.gax.engine.model.EngineCreator;
import com.gantang.gax.engine.model.VariableGroup;
import com.gantang.gax.engine.service.LogicEngineService;
import com.gantang.gax.engine.utils.NameConversionTool;
import com.gantang.gax.engine.utils.StrUtils;
import lombok.Data;
import lombok.EqualsAndHashCode;
import org.logicng.datastructures.Assignment;
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Variable;
import org.logicng.io.parsers.FormulaParser;
import org.logicng.io.parsers.ParserException;
import org.logicng.io.parsers.PseudoBooleanParser;
import org.logicng.modelcounting.ModelCounter;
import org.logicng.propositions.Proposition;
import org.logicng.propositions.StandardProposition;
import org.logicng.solvers.MaxSATSolver;
import org.logicng.solvers.MiniSat;
import org.logicng.solvers.SATSolver;
import org.logicng.solvers.SolverState;
import org.logicng.solvers.maxsat.algorithms.MaxSAT;
import org.logicng.solvers.sat.MiniSatConfig;

import java.math.BigInteger;
import java.util.*;
import java.util.stream.Collectors;

@Data
@EqualsAndHashCode(callSuper = true)
public class LogicEngine extends Engine implements LogicEngineService {
    public static final String INTERNAL_RULES = "内部自定规则";
    public static final String MUST_SELECTED_RULES_DISPLAY_NAME = "已选";
    public static final String BAN_SELECTED_RULES_DISPLAY_NAME = "没选";
    public static final String FAMILY_RULES_DISPLAY_NAME = "家族约束";
    protected Long maxSolutionLimitation = -1l;  //查找排列组合枚举的最大数量限制，避免可行组合过多导致时间和内存资源消耗过大，-1为不限制
    protected Long currentSolutionCount = 0l;
    protected Long maxSolutionDuration = -1l;  //查找排列组合枚举的最大时间限制，单位毫秒，避免可行组合过多导致时间消耗过大，-1为不限制

    protected final String XOR_OPERATOR_SEARCH = "<|>";   //表达式对于异或的特殊操作符
    protected final String XOR_OPERATOR_REPLACE = "<=>~"; //经过转换的异或内部表达式操作符

    protected FormulaFactory formulaFactory = null;
    protected SATSolver miniSat = null;
    protected MaxSATSolver maxSat = null;
    protected SolverState state = null;
    protected FormulaParser parser = null;


    protected NameConversionTool nameConversionTool = null; //外部输入的特征族和值的编码命名往往不是很规范，该工具进行标准化命名替换
    protected Map<String, List<String>> familyMap = null; //外部输入的初始特征家族信息
    protected Map<String, String> featureFamilyMap = null; //根据外部输入的特征家族信息，建立从特征值到家族的反向映射关系
    protected List<String> featureRuleList = null;   //外部输入的初始约束规则信息
    protected Map<String, String> featuresNaming = null; // 特征值与特征名称映射
    protected List<Formula> initialFormulaList = null;   //根据初始输入转换的公式集
    protected List<Proposition> initialPropositionList = null;    //根据初始输入转换的命名公式集
    protected List<Formula> appendFormulaList = new ArrayList<>();

    protected Boolean timerLog = true; //是否打印性能计时日志信息
    protected Boolean needPossibleCombination = false;  //是否需要近似的解提供

    protected TimeInterval currentSolutionBeginTimer = null;

    SortedSet<Variable> variables = new TreeSet<>(); //所有输入的特征值都会定义为变量

    /**
     * @param familyMap               以家族编码为Key的特征值信息，特征值编码需全局唯一。
     * @param featureRuleList         约束条件集，这些条件都是必须满足的。
     * @param featuresNaming          特征值的业务显示名称，用于输出信息展示
     * @param needPossibleCombination 是否需要近似的解提供，如果为true，会初始化一个MaxSat引擎，用于计算近似解
     * @param timerLog                是否需要打印性能计时日志信息
     */
    public LogicEngine(Map<String, List<VariableGroup.Variable>> familyMap, List<String> featureRuleList, Map<String, String> featuresNaming,
                       Boolean needPossibleCombination, Boolean timerLog) throws EngineException {

        cardsDeductionEngine_pri(familyMap, featureRuleList, featuresNaming,
                needPossibleCombination, timerLog);

    }

    private void cardsDeductionEngine_pri(Map<String, List<VariableGroup.Variable>> familyMap, List<String> featureRuleList, Map<String, String> featuresNaming,
                                          Boolean needPossibleCombination, Boolean timerLog) throws EngineException {

        this.nameConversionTool = new NameConversionTool(); //外部各种家族和值的名称定义不规范，通过命名工具进行统一转换处理

        this.familyMap = nameConversionTool.familyNameConvert2(familyMap);
        this.featureRuleList = (null == featureRuleList) ? new ArrayList<String>() : nameConversionTool.rulesConvert(featureRuleList);
        this.featuresNaming = nameConversionTool.featureDisplayNameConvert(featuresNaming);
        this.needPossibleCombination = needPossibleCombination;
        this.timerLog = timerLog;

        TimeInterval timer = DateUtil.timer();

        this.prepareMiniLogicEngine();
        if (needPossibleCombination) {
            this.prepareMaxLogicEngine();
        }
        log("创建逻辑规则引擎耗时{}毫秒", timer.intervalRestart());

        this.prepareRules();
        log("添加规则到推导器耗时{}毫秒", timer.interval());

    }

    /**
     * 准备阶段，准备好底层所依赖的MiniSat逻辑推导引擎
     */
    private void prepareMiniLogicEngine() {
        formulaFactory = new FormulaFactory();
        MiniSatConfig miniSatConfig = MiniSatConfig.builder().proofGeneration(true).build();
        miniSat = MiniSat.miniSat(formulaFactory, miniSatConfig);

//        GlucoseConfig glucoseConfig = GlucoseConfig.builder().build();
//        miniSat = MiniSat.glucose(formulaFactory, miniSatConfig, glucoseConfig);

//        miniSat = MiniSat.miniCard(formulaFactory, miniSatConfig);

        parser = new PseudoBooleanParser(formulaFactory);
    }

    /**
     * 准备阶段，准备好底层所依赖的MaxSat逻辑推导引擎
     */
    private void prepareMaxLogicEngine() {
//        maxSat = MaxSATSolver.incWBO();

//        maxSat = MaxSATSolver.wmsu3(formulaFactory);

        maxSat = MaxSATSolver.oll(formulaFactory);
    }

    /**
     * 准备阶段，将约束规则解析成为公式，所有初始的约束条件加入到推导引擎中
     *
     * @throws EngineException 解析失败异常信息
     */
    private void prepareRules() throws EngineException {
        initialFormulaList = new ArrayList<>();
        initialPropositionList = new ArrayList<>();

        //每个家族的特征值仅可以选一个，添加默认约束规则exo（exactly one）， 所有特征值都定义为变量
        for (Map.Entry<String, List<String>> entry : familyMap.entrySet()) {
            String family = entry.getKey();
            List<String> familyFeatures = entry.getValue();
            ArrayList<Variable> familyVars = new ArrayList<>();
            for (String feature : familyFeatures) {
                Variable featureVar = formulaFactory.variable(feature);
                familyVars.add(featureVar);
                variables.add(featureVar);
            }
            Formula familyExoFormula = formulaFactory.exo(familyVars);
            StandardProposition proposition = new StandardProposition(nameConversionTool.anyNameConvert(family) + FAMILY_RULES_DISPLAY_NAME, familyExoFormula);
            initialFormulaList.add(familyExoFormula);
            initialPropositionList.add(proposition);
            miniSat.add(proposition);
            if (needPossibleCombination) {
                maxSat.addHardFormula(familyExoFormula);
            }
        }

        //加入定义的特征值间约束规则
        try {
            for (String rule : featureRuleList) {
                Formula formula = parser.parse(replaceOperator(rule));
                StandardProposition proposition = new StandardProposition(getDescription(rule), formula);
                initialFormulaList.add(formula);
                initialPropositionList.add(proposition);
                miniSat.add(proposition);
                if (needPossibleCombination) {
                    maxSat.addHardFormula(formula);
                }
            }
            state = miniSat.saveState();
        } catch (ParserException e) {
            throw new EngineException(e.getCause());
        }

    }


    /**
     * 获取配置描述
     *
     * @param convertedRule 已经标准化命名的规则
     * @return 描述
     */
    private String getDescription(String convertedRule) {
        if (StrUtil.isEmpty(convertedRule)) {
            return null;
        }

        String rule = nameConversionTool.ruleConvert(convertedRule);
        String convertedFeatureName = convertedRule;
        String featureName = rule;
        boolean mustSelectedFlag = true;

        if (convertedRule.startsWith("!")) {
            convertedFeatureName = convertedRule.substring(1);
            featureName = rule.substring(1);
            mustSelectedFlag = false;
        }

        String featureDisplayName = featuresNaming.get(convertedFeatureName);

        //如果featureDisplayName为空，则说明这应该是一条规则
        if (null == featureDisplayName) {
            return rule;
        } else {
            return featureDisplayName + "[" + featureName + "]" + (mustSelectedFlag ? MUST_SELECTED_RULES_DISPLAY_NAME : BAN_SELECTED_RULES_DISPLAY_NAME);
        }
    }

    protected void log(String template, Object... objects) {
        if (timerLog) {
            Console.log(template, objects);
        }
    }

    protected String replaceOperator(String rule) {
        return replaceOperator_pri(rule);
    }

    private String replaceOperator_pri(String rule) {
        if (StrUtil.isBlank(rule)) {
            return rule;
        }
        //额外的一个转换，原先规则中使用感叹号的需要调整为波浪号
        rule = StrUtils.replaceChar(rule, '!', '~');
//        rule = StrUtil.replace(rule, "!", "~");

        if (!StrUtil.contains(rule, XOR_OPERATOR_SEARCH)) {
            return rule;
        }
        String[] subRuleArray = StrUtil.splitToArray(rule, XOR_OPERATOR_SEARCH);

        StringBuffer resultBuffer = new StringBuffer();
        for (int i = 0; i < subRuleArray.length; i++) {
            resultBuffer.append("(" + subRuleArray[i] + ")");
            if (i < (subRuleArray.length - 1)) {
                resultBuffer.append(XOR_OPERATOR_REPLACE);
            }
        }
        return resultBuffer.toString();
    }

    @Override
    public void reset() {
        TimeInterval timer = DateUtil.timer();
        if (null != state) {
            miniSat.loadState(state);
        }
        // 还原时清空追加的表达式
        appendFormulaList.clear();

        if (needPossibleCombination) {
            maxSat.reset();
            for (Formula formula : initialFormulaList) {
                maxSat.addHardFormula(formula);
            }
        }
        log("恢复推导引擎到初始化状态耗时{}毫秒", timer.interval());
    }

    @Override
    public BigInteger solutionCount() {
        List<Formula> formulaList = new ArrayList<>(initialFormulaList);
        formulaList.addAll(appendFormulaList);
        return ModelCounter.count(formulaList, variables);
    }

    public boolean validateHardRules() {
        if (needPossibleCombination) {
            TimeInterval timer = DateUtil.timer();
            MaxSAT.MaxSATResult result = maxSat.solve();
            log("验证优化可选规则逻辑耗时{}毫秒", timer.interval());
            switch (result) {
                case UNSATISFIABLE:
                    return false;
                case UNDEF:
                    return false;
                default:
                    return true;
            }
        } else {
            throw new EngineException("当前不支持该功能");
        }
    }

    @Override
    public List<String> findBestSolution() {
        if (needPossibleCombination) {
            if (validateHardRules()) {
                TimeInterval timer = DateUtil.timer();
                Assignment assignment = maxSat.model();
                log("获取一个尽可能满足的解耗时{}毫秒", timer.interval());
                // 过滤掉内部变量
                List<String> internalSolution = assignment.positiveVariables().stream().map(Variable::name)
                        .filter(it -> !it.startsWith(FormulaFactory.CC_PREFIX)).collect(Collectors.toList());
                return nameConversionTool.getNameMappingByList(internalSolution);

            } else {
                throw new EngineException("强制规则不满足，无法找到近似解");
            }
        } else {
            throw new EngineException("当前不支持该功能");
        }
    }

    @Override
    public BigInteger solutionCount2() {
        return this.solutionCount();
    }
}
